1. Field of the Invention
The automation of interface timing verification is important for the design of reliable systems composed of several interconnected components. Due to manufacturing or environmental variation, the delay between two signal transitions of a component may not be a precise number, and is usually specified with a lower bound and an upper bound by the manufacturers. Exhaustive simulation, where all possible combinations of delay values are checked, is impractical for large systems. Therefore, efficient analytical verification algorithms are necessary to ensure that all timing requirements will be satisfied for all possible delay values.
2. Description of the Related Art
A convenient means for describing the timing interaction of signals and events is a timing diagram. A timing diagram is a set of signals, where each signal is composed of signal edges which represent events in time such as a transition from high to low, transition from high impedance to driven, etc. The time position of events in the timing diagram is determined by timing constraints between events. A constraint [cij] (meaning a constraint between events i and j) in general has a lower bound component, lower cij, and an upper bound component, upper cij. There are many possible timing constraints between signal events with various semantic definitions, but only two types, the most common in practice, are considered here:
linear,                     max        i            ⁢              (                              time            ⁡                          [              i              ]                                +                      lower            ⁡                          [                              c                ij                            ]                                      )              ≤          time      ⁡              [        j        ]              ≤                  min        i            ⁢                        (                                    time              ⁡                              [                i                ]                                      +                          upper              ⁡                              [                                  c                  ij                                ]                                              )                ⁢                  xe2x80x83                ⁢        and        ⁢                  xe2x80x83                ⁢        max              ,                    max        i            ⁢              (                              time            ⁡                          [              i              ]                                +                      lower            ⁡                          [                              c                ij                            ]                                      )               less than =          time      ⁡              [        j        ]               less than =                  max        i            ⁢                        (                                    time              ⁡                              [                i                ]                                      +                          upper              ⁡                              [                                  c                  ij                                ]                                              )                .            
In a practical context, guarantees and requirements are linear constraints and delays are max constraints.
Note that only maximum separations need be calculated, because minimum separations can be calculated by:
min(time[i]xe2x88x92time[j])=xe2x88x92max(time[j]xe2x88x92time[i]).
A timing diagram is modeled by an event graph whose nodes represent events and whose weighted directed edges are timing constraints, either linear or max. Each edge is labeled with both the lower bound and upper bound component associated with the edge.
One of the shortcomings of currently available commercial tools is that they either do not deal with guarantees and requirements, or, if they do, the results are frequently incorrect or unreliable. Many commercial tools are based on a timing analysis engine that handles only max or min timing relationships. This limits the application of these tools for describing timing guarantees, signal tracking and clock jitter, all of which require linear constraints as well as max constraints. Also, the inability to use linear constraints prevents the possibility of error diagnosis capability in timing analysis.
A previous paper, xe2x80x9cEfficient Algorithms for Interface Timing Verification,xe2x80x9d T.-Y. Yen, A. Ishii, A. Casavant, and W. Wolf, Proceedings, European Conference on Design Automation, (EDAC), 1994, pp. 34-39, describes an algorithm for performing timing verification in designs having minimum and maximum event separations expressed using max and linear timing relationships. This algorithm is known as the xe2x80x9cMax-Plus-Linearxe2x80x9d (hereinafter, xe2x80x9cMPLxe2x80x9d) Algorithm, and is described in more detail below.
Since the present invention is primarily concerned with the MPL algorithm, previous work in the algorithm area will just be touched on. However, general work in the area can be found in xe2x80x9cSolving Linear, Min and Max constraint Systems Using CLP based on Relational Interval Arithmetic,xe2x80x9d P. Girodias, E. Cerny, and W. J. Older, Theoretical Computer Science, 1997, Vol. 173, No. 1, February, pp. 253-281; xe2x80x9cInterface Timing Verification with Delay Correlation Using Constraint Logic Programming,xe2x80x9d P. Girodias, E. Cerny, Proceedings of the European. Design and Test Conference, 1997. pp. 12-19; xe2x80x9cHigh-Level Timing Analysis using Constraint Logic Programming and Interval Arithmetic,xe2x80x9d P. Girodias and E. Cerny, Proceedings of the Canadian Conference on Electrical and Computer Engineering, Vol. 2, 1995, pp. 636-639; xe2x80x9cModeling and Execution of Timing Diagrams and Multi-Match Events,xe2x80x9d K. Khordoc, E. Cerny, and M. Dufresne, TAU ""92; xe2x80x9cAlgorithms for Interface Timing Verification,xe2x80x9d K. L. McMillan and D. L. Dill, Proceedings of IEEE International Conference on Computer Design (ICCD), 1992, pp. 48-51; xe2x80x9cVerification of Asynchronous Circuits Using Time Petri Net Unfolding,xe2x80x9d A. Semenov and A. Yakovlev, Proceedings of ACM IEEE Design Automation Conference, 1996, pp. 59-62; xe2x80x9cSpecification and Analysis of Timing Constraints in Signal Transition Graphs,xe2x80x9d P. Vanbekbergen, G. Goossens, and H. DeMan, Proceedings, European Conference on Design Automation, (EDAC), 1992, pp. 302-306.
Work specifically in the max plus linear realm can be found in xe2x80x9cInterface Timing Verification With Application to Synthesis,xe2x80x9d E. A. Walkup and G. Boriello, Proceedings, Design Automation Conference, (DAC), 1994, pp. 106-112; xe2x80x9cAlgorithms for Interface Timing Verification,xe2x80x9d K. L. McMillan and D. L. Dill, Proceedings of IEEE International Conference on Computer Design (ICCD), 1992, pp. 48-51.
Work in the cyclic version of max plus linear is in xe2x80x9cAn Algorithm for Exact Bounds on the Time Separation of Events in Concurrent Systems,xe2x80x9d T. Amon, H. Hulgaard, S. M. Bums, and G. Borriello, Proceedings, IEEE International Conference on Computer Design, (ICCD), 1993, pp. 166-173; xe2x80x9cEfficient Timing Analysis of a Class of Petri Nets.xe2x80x9d H. Hulgaard and S. M. Burns, CAV ""95, LNCS 939; xe2x80x9cMaximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints,xe2x80x9d F. Jin. H. Hulguard, E. Cerny, FMCAD ""98.
The details of the MPL algorithm and outlines of proofs can be found in xe2x80x9cEfficient Algorithms for Interface Timing Verification,xe2x80x9d mentioned above. Here, a brief overview of the MPL algorithm will be given to provide background for the following discussion of the invention.
In FIG. 1, the initialization step uses a single source longest path algorithm (Bellman-Ford algorithm) described in Chapter 25 of Introduction to Algorithms, T. H. Cormen, C. E. Leiserson, and R. L. Rivest, McGraw Hill, 1990. In the Iterative Adjustment Step, on each iteration, a slack graph is constructed. The nodes in the slack graph are events, as in the event graph. The edges, however, represent the available slack between two events.
FIG. 2 defines bound satisfaction for upper and lower bounds. In the upper portion of FIG. 2, events A and B occur at event times ta and tb, respectively. If the difference between tb and ta is less than or equal to a particular upper bound, then that upper bound is satisfied. Similarly, in the lower portion of FIG. 2, the difference between tb and ta must be greater than or equal to a particular lower bound for that bound to be satisfied.
The slack calculation for a lower bound of a max or linear constraint is shown boxed on the left of FIG. 3. All lower bounds, whether associated with linear constraints or max constraints are compulsory, meaning that they must always be satisfied.
The slack calculation for an upper bound of a max or linear constraint is shown boxed on the right of FIG. 3. The upper bounds of linear constraints are compulsory, but the upper bounds of max constraints are max-optional. Max-optional bounds may or may not be satisfied on a constraint by constraint basis. Slacks of compulsory bounds and satisfied upper bounds of max constraints have positive slack and become edges in the slack graph. In a consistent solution, at least one of the max optional bounds entering an event must be satisfied.
The shortest slack xcex4[i] is calculated as the minimum of the compulsory slack xcex4c[i] and the max-optional slack xcex4m[i] as shown in FIG. 3. A procedure based on Dijkstra""s shortest path algorithm (Chapter 25 in Introduction to Algorithms) for calculating the shortest slack is shown in FIG. 4. The difference between ShortestSlack and the Dijkstra algorithm is within the conditional . . . IF (eui is optional) . . .
In FIG. 4, t is the sum of the estimated slack of event u, d[u], and the available positive slack (weight of the edge in the slack graph). For a compulsory edge, if t is greater then the slack of event i (d([i]), then event i""s slack is updated. For a max-optional edge, a running calculation of the maximum t found so far among all max-optional edges entering i is kept by m[i]. When the last max-optional edge is encountered, d[i] is updated. Note that d[i] is always set to guarantee satisfaction for all compulsory edges but only the maximum of the max-optional edges entering an event. If the priority queue is implemented with a Fibonacci heap, the complexity of ShortestSlack is O(V log V+E) where V is the number of nodes and E is the number of edges in the event graph. After running ShortestSlack, xcex4[u] (the actual shortest slack from source node to u) for all nodes u=d[u] (the estimate of shortest slack from source node to u).
FIG. 5 shows the MaxSeparation (iterative adjustment) algorithm. After new xcex4[u]s are calculated, the event separations are adjusted to reflect those results. When this occurs, the slack graph previously calculated is no longer accurate and must be updated. This is done on each iteration of MaxSeparation. Some edges that were in the old slack graph are not in the new one and some edges which were not in the old slack graph are in the new one. If there is no increase in event separations on an iteration of MaxSeparation, the algorithm terminates.
Infeasibility arises if a compulsory upper bound between two events is smaller than some sequence of lower bounds between the same two events. Inconsistency arises where a lower bound of a linear constraint or a sequence of lower bounds ending in the lower bound of a linear constraint, prevents the satisfaction of any of the upper bounds of the max constraints entering an event. Another possibility is a missing upper bound on a max constraint which allows separations to increase indefinitely. Infeasibility is tested during the initialization phase as shown in FIG. 5. Inconsistency is checked in MaxSeparation as shown in FIG. 5.
It is an object of the present invention to provide a method and system for performing interface timing analysis, primarily at the chip macro level of IC design, or at the board level, or the gate level, which performs provably correct timing analysis. The invention implements the MPL algorithm to achieve this object and other objects as discussed below.
It is a further object of the invention to identify all violations of timing constraints within a desired operation of a particular circuit, and to overcome these constraint violations by setting a guaranteed value for them. Cumulative delays which are created earlier in the circuit operation as a result of this object of the invention are absorbed by the strategic replacement or redesign of the circuit(s) in question.
It is a still further object of the invention to increase circuit design flexibility by taking advantage of events which occur within a certain time period of one another, due to environmental parameters of the circuit such as process, voltage and/or temperature variations. The invention accomplishes this object by designating such a set of events, and thereafter constraining each event within the set of events so that their relative delays are a set and known quantity. These events can include, but are not limited to, events such as those which vary according to a duty cycle variation of a clock phase generator and/or clock buffer delays.